A, B:MsgA, x:Id.
A || B
 (k:Knd, s:A.state, v:A.da(k). ma-ef-const(A;k;x;s;v))
 (k:Knd, s:B.state, v@0:B.da(k). ma-ef-const(B;k;x;s;v@0))
 (k:Knd, s:A  B.state, v:A  B.da(k). ma-ef-const(A  B;k;x;s;v)) 

latex

Definitions

x:A  B(x), P & Q, M1 || M2, Knd, Id, State(ds), Type, t.1, Top, f(x)?z, , t.2, Void, x:AB(x), <a, b>, f(x), f(a), IdDeq, f  g, s = t, x:A. B(x), t  T, b, A, b, , , x.A(x), x. t(x), KindDeq, a:A fp B(a), product-deq(A;B;a;b), x  dom(f), P  Q, P  Q, Unit, left + right, x:A.B(x), False, P  Q, z != f(x)  P(a;z), constant_function(f;A;B), M1 ||decl M2, Valtype(da;k), M.ds(x), mk-ma, MsgA, ma-ef-const(M;k;x;s;v), M.da(a), M.state, M1  M2, Atom$n, f || g, if b then t else f fi , x,y:A//B(x;y), f  g, True, T, IdLnk, x(s), EqDecider(T), s ~ t, {T}, SQType(T), case b of inl(x) => s(x) | inr(y) => t(y), , Dec(P)

Lemmas

decidable assert, fpf-sub-join-right, fpf-join-cap-sq, false wf, subtype rel self, fpf-ap wf, subtype-fpf-cap-void, deq wf, IdLnk wf, subtype-fpf-cap-top, fpf-sub-join-left, squash wf, true wf, fpf wf, ma-state-subtype, fpf-sub-join-left2, fpf-sub weakening, ma-join wf, ma-st wf, ma-da wf, ma-ef-const wf, ma-compatible wf, msga wf, fpf-join wf, fpf-join-dom2, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, product-deq wf, fpf-trivial-subtype-top, ma-state wf, Kind-deq wf, pi1 wf, top wf, rationals wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, Id wf, bool wf, bnot wf, not wf, assert wf